Inference at * 1 1 2 1 1 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. i : {0..(||L1 @ L2|| - 1)}
7. x = L1[i]
8. y = L2[((i+1) - ||L1||)]
9. i < ||L1||
10. (i < (||L1|| - 1))
  x = last(L1) 

latex

 by ((HypSubst (-4) 0) 
CollapseTHENA (((Auto) 
CollapseTHEN (((DVar `L1') 
CollapseTHEN (((
CAll Reduce) 
CollapseTHEN (Auto)))))))) 

latex

C1: 

C1:   L1[i] = last(L1)
C.

Definitions	last(L), x:A. B(x), null(as), True, -n, b, {x:A| B(x)} , , i  j < k, A  B, P & Q, Void, P  Q, x:AB(x), n - m, n+m, ||as||, #$n, , l[i], [car / cdr], A, a < b, {i..j}, type List, Type, False, t  T, s = t
Lemmas	last wf, assert wf, true wf, not wf, false wf